Automated theorem proving

Automated theorem proving (ATP) or automated deduction, currently the most well-developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program.

Contents

Decidability of the problem

Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but Co-NP-complete, and hence only exponential-time algorithms are believed to exist for general proof tasks. For a first order predicate calculus, with no ("proper") axioms, Gödel's completeness theorem states that the theorems (provable statements) are exactly the logically valid well-formed formulas, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven.

However, invalid formulas (those that are not entailed by a given theory), cannot always be recognized. In addition, a consistent formal theory that contains the first-order theory of the natural numbers (thus having certain "proper axioms"), by Gödel's incompleteness theorem, contains true statements which cannot be proven. In these cases, an automated theorem prover may fail to terminate while searching for a proof. Despite these theoretical limits, in practice, theorem provers can solve many hard problems, even in these undecidable logics.

Related problems

A simpler, but related, problem is proof verification, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable.

Interactive theorem provers require a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Interactive provers are used for a variety of tasks, but even fully automatic systems have proven a number of interesting and hard theorems, including some that have eluded human mathematicians for a long time.[1][2] However, these successes are sporadic, and work on hard problems usually requires a proficient user.

Another distinction is sometimes drawn between theorem proving and other techniques, where a process is considered to be theorem proving if it consists of a traditional proof, starting with axioms and producing new inference steps using rules of inference. Other techniques would include model checking, which is equivalent to brute-force enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force).

There are hybrid theorem proving systems which use model checking as an inference rule. There are also programs which were written to prove a particular theorem, with a (usually informal) proof that if the program finishes with a certain result, then the theorem is true. A good example of this was the machine-aided proof of the four color theorem, which was very controversial as the first claimed mathematical proof which was essentially impossible to verify by humans due to the enormous size of the program's calculation (such proofs are called non-surveyable proofs). Another example would be the proof that the game Connect Four is a win for the first player.

Industrial uses

Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. Since the Pentium FDIV bug, the complicated floating point units of modern microprocessors have been designed with extra scrutiny. Nowadays, AMD, Intel and others use automated theorem proving to verify that division and other operations are correctly implemented in their processors.

First-order theorem proving

First-order theorem proving is one of the most mature subfields of automated theorem proving. The logic is expressive enough to allow the specification of arbitrary problems, often in a reasonably natural and intuitive way. On the other hand, it is still semi-decidable, and a number of sound and complete calculi have been developed, enabling fully automated systems. More expressive logics, such as higher order logics, allow the convenient expression of a wider range of problems than first order logic, but theorem proving for these logics is less well developed.

Benchmarks and competitions

The quality of implemented system has benefited from the existence of a large library of standard benchmark examples — the Thousands of Problems for Theorem Provers (TPTP) Problem Library[3] — as well as from the CADE ATP System Competition (CASC), a yearly competition of first-order systems for many important classes of first-order problems.

Some important systems (all have won at least one CASC competition division) are listed below.

Popular techniques

Comparison

See also: Proof assistant#Comparison and Category:Theorem proving software systems

Name License type Web service Library Standalone Version Last update Author
Prover9 / Mace4 GPLv2 No Yes Yes v05 11/2009 William McCune / Argonne National Laboratory
Otter Public Domain Via System on TPTP Yes No - 09/2004 William McCune / Argonne National Laboratory
j'Imp ? No No Yes - 05/28/2010 André Platzer
Metis ? No Yes No 2.2 05/24/2010 Joe Hurd
Jape ? Yes Yes No 1.0 03/22/2010 Adolfo Gustavo Neto, USP
PVS ? No Yes No 4.2 07/2008 Computer Science Laboratory of SRI International, California, USA
Leo II  ? Via System on TPTP Yes Yes 1.2.8 2011 Christoph Benzmüller, Frank Theiss, Larry Paulson. FU Berlin and University of Cambridge
EQP ? No Yes No 0.9e May/2009 William McCune / Argonne National Laboratory
SAD ? Yes Yes No 2.3-2.5 08/27/2008 Alexander Lyaletski, Konstantin Verchinine, Andrei Paskevich
PhoX ? No Yes No 0.88.100524 - Christophe Raffalli, Philippe Curmin, Pascal Manoury, Paul Roziere
KeYmaera  ? No Yes No 1.8 06/04/2010 André Platzer, Jan-David Quesel; Philipp Rümmer; David Renshaw
Gandalf ? No Yes No 3.6 2009 Matt Kaufmann e J. Strother Moore, Universidade de Texas em Austin
Tau ? No Yes No - 2005 Jay R. Halcomb e Randall R. Schulz da H&S Information Systems
E GPL Via System on TPTP No Yes E 1.2 10/24/2010 Stephan Schulz, Automated Reasoning Group, Technical University of Munich
SNARK Mozilla Public License No Yes No snark-20080805r018b 2008 Mark E. Stickel
Vampire/Vampyre ? No Yes No Third re-incarnation Vampire 2008 Andrei Voronkov, Alexandre Riazanov, Krystof Hoder
Waldmeister  ? Yes Yes No - - Thomas Hillenbrand, Bernd Löchner, Arnim Buch, Roland Vogt, Doris Diedrich
Saturate ? No Yes No 2.5 10/1996 Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela Pilar Nivela
Theorem Proving System (TPS) ? No Yes No - 06/24/2004 Carnegie Mellon University
SPASS ? Yes Yes Yes 3.7 11/2005 Max Planck Institut Informatik
IsaPlanner GPL No Yes Yes IsaPlanner 2 2007 Lucas Dixon, Johansson Moa
KeY GPL Yes Yes Yes 1.6 10/2010 Karlsruhe Institute of Technology, Chalmers University of Technology, University of Koblenz
ACL2 ? No No Yes 4.1 09/2010 Matt Kaufmann, J. Strother Moore
Theorem Checker ? Yes No No 0 2010 Robert J. Swartz, Northeastern Illinois University

Free software

Proprietary Software

Notable people

See also

Notes

  1. ^ W.W. McCune (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning 19 (3). http://www.springerlink.com/content/h77246751668616h/. 
  2. ^ Gina Kolata (December 10, 1996). "Computer Math Proof Shows Reasoning Power". The New York Times. http://www.nytimes.com/library/cyber/week/1210math.html. Retrieved 2008-10-11. 
  3. ^ http://www.cs.miami.edu/~tptp/
  4. ^ http://www.csl.sri.com/users/rushby/

References